#ifndef KLEE_CHANGE_MACROS_H_
#define KLEE_CHANGE_MACROS_H_

#include <stdio.h>
#include <stdlib.h>

#ifndef RESOLVE_KLEE_CHANGE
#define RESOLVE_KLEE_CHANGE 1
#endif

#if RESOLVE_KLEE_CHANGE == 0
#include <stdint.h>

int after_divergence = 0;
const char* klee_div_file_env="KLEE_DIVERGENCE_FILE";
const char* klee_div_marker_file_env="EKLEEPSE_MARKER_FILE";

uintptr_t klee_change(uintptr_t x, uintptr_t y) { 
  if (x == y)
    return x;
  else { // concrete div
    if (!after_divergence) {
      // get the name of the file where we account for divergences; this is kept
      // in an env variable
      char* file = getenv(klee_div_file_env);
      char* marker_file = getenv(klee_div_marker_file_env);

      if (file) {
        // append a new line to the file, so that we know how many divergences
        // we hit
        FILE* f = fopen(file, "a");
        if (f) {
          fprintf(f, "1\n");
          fflush(f);
          fclose(f);
        }
        else {
          fprintf(stderr, "fopen failed for file %s\n", file);
        }
        if (marker_file) {
          f = fopen(marker_file, "w");
          if (f) {
            fflush(f);
            fclose(f);
          }
          else {
            fprintf(stderr, "fopen failed for file %s\n", file);
          }
        }
        else {
          fprintf(stderr, "getenv failed for key %s\n", klee_div_marker_file_env);
        }

      }
      else {
        fprintf(stderr, "getenv failed for key %s\n", klee_div_file_env);
      }
      // mark that we've already hit a concrete divergence
      after_divergence = 1;
    }
    return y;
  }
  
}
#endif

// RESOLVE_KLEE_CHANGE: 
// case -1: use old version
// case  1: use new version
// case  0: use both when ran with KLEE (for future use)
#define klee_change(x,y) (((RESOLVE_KLEE_CHANGE) == -1) ? (x) : ( ((RESOLVE_KLEE_CHANGE) == 1)  ? (y) : (klee_change(x,y))) )

#endif /* KLEE_CHANGE_MACROS_H_ */
